\Aufgabe[Predicate Abstraction\hfill\textbf{(1.5 Point)}]
Consider the following program:
\begin{verbatim}
void foo(int j, int z) {
  assume(z != 0);
  int i := j;
  while(z != 0) {
      i := i + z;
      if(z > 0)
          z--
      else
          z ++;
  };
  assert(i != j)
}
\end{verbatim}

The {\em assume statement} at the beginning of the function forces the parameter $z$ not to be 0 when the function is called.

\begin{enumerate}

 \item Argue in your own words why the assertion at the end of the program allways holds, i.e., why the error state can never be reached.

 \item Provide a labeled transition system for the given program.

 \item Provide an abstraction for the labeled transition system that uses the predicates $i = j$, $i < j$, $i > j$.

 \item Check whether the error state can be reached in the abstraction, if so state a trace to the error state and refine the abstraction with suitable predicates such that the error state is not reachable anymore.

\end{enumerate}

\textbf{Solution}

a) The program computes: 
\begin{center}
	$i = j + z + (z-1) + (z-2) + \ldots + 1$ if $z > 0$\\
	$i = j + z + (z+1) + (z+2) + \ldots - 1$ if $z < 0$
\end{center}
Since z cannot be 0 due to the call to assume(), $ i \neq j$ must hold in both cases.\\

b) The LTS for the program is shown in Figure 1.\\

\begin{figure}
	\centering
		\includegraphics[scale=0.25]{5b_lts.jpg}
	\caption{Labeled Transition System}
	\label{fig:5b_lts}
\end{figure}

c) The abstraction for the labeled transition system is shown in Figure 2. To keep the graph smaller, the state transitions from 6 to 10 have been merged into one state, as those states have the same predicates.\\

\begin{figure}
	\centering
		\includegraphics[scale=0.25]{5c_abstraction.jpg}
	\caption{Abstraction for the LTS}
	\label{fig:5c_abstraction}
\end{figure}

d) In the abstraction, is it possible to arrive at the error-state E. One possible trace is: 1, 2, 3, 11, E. In the refined abstraction provided in Figure 3, there is no way to reach the error-state. The newly introduced predicates are: $z = 0$ and $z \neq 0$. Again, some state transitions have been merged.\\

\begin{figure}
	\centering
		\includegraphics[scale=0.22]{5d_refinement.jpg}
	\caption{Refined abstraction}
	\label{fig:5d_refinement}
\end{figure}